A:Type, eq:EqDecider(A), B:(AType), P, Q:(A), f:x:A fp B(x).
filter(pL.Q(1of(pL));fpf-vals(eq;P;f)) ~ fpf-vals(eq;a.P(a)  Q(a);f) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), , x(s), x. t(x), a:A fp B(a), let x = a in b(x), fpf-vals(eq;P;f), P  Q, remove-repeats(eq;L), (x  l), strong-subtype(A;B), P  Q, P & Q, P  Q, P  Q, Prop, {T}, filter(P;l), Unit, zip(as;bs), if b t else f fi
Lemmas	subtype rel list, cons member, strong-subtype-deq-subtype, strong-subtype-set3, strong-subtype-self, remove-repeats wf, l member wf, fpf wf, bool wf, deq wf